(declare-fun a () Int)
(declare-fun b (Int Int) Bool)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun h () Bool)
(assert (forall ((g Int) (j Int)) (=> (<= 1 g (div a d)) (forall ((i Int) (k Int)) (= (b j i) (<= k i))))))
(assert (ite h (and (= (div a c) (str.len f)) (= f "utm_id=")) (distinct e "")))
(assert (= a c (div a d)))
(check-sat)
